Lean 语言参考手册

5. 源文件与模块🔗

在 Lean 中，编译的最小单位是单个 模块。 模块对应于源代码文件，并且可以按文件名被其他模块导入。 换句话说，文件的名称和文件夹结构在 Lean 代码中具有重要意义。

每个 Lean 文件都定义一个模块。 模块名称由其文件名以及 Lean 启动时的方式共同决定：Lean 有一个根目录，它期望在该根目录下找到代码，模块的名称则是从根目录到文件名各级目录的名称，用点（.）隔开，并去掉 .lean 后缀。 举例来说，如果 Lean 以 Projects/MyLib/src 作为根目录启动，那么文件 Projects/MyLib/src/Literature/Novel/SciFi.lean 中包含的模块名称就是 Literature.Novel.SciFi。

5.1. 编码与表示🔗

Lean 模块是采用 UTF-8 编码的 Unicode 文本文件。 文件的每一行可以以换行字符（\n，Unicode 'LINE FEED (LF)' (U+000A)）结尾，也可以以回车加换行序列（\r\n，即 Unicode 'CARRIAGE RETURN (CR)' (U+000D) 加 'LINE FEED (LF)' (U+000A)）结尾。 不过，在解析或比较文件时，Lean 会对行尾进行归一化，因此所有文件在比较时都视为全部是 \n 行尾。

5.2. 具体语法🔗

Lean 的具体语法是 可扩展的。 在 Lean 这样的语言中，无法一次性完整地描述所有语法，因为库中还可以定义新的语法、常量，或者 归纳类型。 本节不会详尽描述整个语言，而是介绍整体框架；各个语言结构的具体语法则在其各自章节中详细说明。

5.2.1. 空白符🔗

Lean 中的词法单元（token）之间可以用任意数量的 空白符 字符序列分隔。 空白符可以是空格 (" ", Unicode 'SPACE (SP)' (U+0020))、合法的换行序列，或注释。 制表符和单独的回车（CR，未跟随换行）不是合法的空白符序列。

5.2.2. 注释🔗

注释是文件中虽然不是空白符，但被视为空白的部分。 Lean 提供两种注释语法：

行注释

当 -- 不作为其他词法单元一部分出现时，表示行注释。该标记后的所有内容直到行尾都会被视为空白字符。

块注释

当 /- 不作为其他词法单元一部分，且后面不是 - 字符时，表示块注释的开始。 块注释会一直持续到出现 -/ 终止为止。 块注释允许嵌套；仅在所有内部嵌套的 /- 都被匹配的 -/ 终止后，最外层才算结束。

/-- 与 /-! 用于开始 文档注释 ，它们同样以 -/ 结束，并允许嵌套块注释。 尽管文档注释看起来与普通注释类似，但在语法上它们属于不同类别；它们能出现的位置由 Lean 的语法决定。

5.2.3. 关键字与标识符🔗

一个 标识符 由一个或多个标识符成分（component）组成，各部分用 '.' 分隔。

标识符成分 由一个字母或类字母字符或下划线（'_'）开头，后面可以跟零个或多个标识符后续字符。 字母包括英文大小写字母，而类字母字符还包含范围较广的非英语字母脚本，比如 Lean 中广泛采用的希腊字母、以及 Unicode 的字母符号区块（如 ℕ、ℤ 等粗体字符和缩写）。 标识符的后续字符包括字母、类字母字符、下划线（'_'）、感叹号（!）、问号（?）、下标和单引号（'）。 作为例外，单独下划线不是合法的标识符。

标识符成分也可以用一对双 尖引号（'«' 和 '»'）括起来。 这样括起来的成分可以包含除 '»' 之外的任意字符，包括 '«'、. 和换行符。 尖引号本身不计入标识符最终内容，所以 «x» 和 x 是同一个标识符。 而 «Nat.add» 是一个包含一个成分的标识符，而 Nat.add 则包含两个成分。

可能的标识符成分中有一些属于保留关键字。 具体的保留关键字集合取决于当前激活的语法扩展集合，后者又依赖于已导入的模块以及当前打开的 命名空间；因此无法为整个 Lean 语言列举一个完整集合。 在大多数语法环境中，若要用关键字作为标识符成分，必须用尖引号括起来。 在某些环境下（如归纳类型的构造子名称）关键字无需尖引号也能作为标识符使用，这些环境称为 原始标识符 环境。

包含一个或多个 '.' 字符的标识符（因此包含多个标识符成分）被称为 分层标识符。 分层标识符同时用于表示模块名称和命名空间中的名称。

5.3. 结构🔗

syntaxModules
Parser for a Lean module. We never actually run this parser but instead use the imperative definitions below that
return the same syntax tree structure, but add error recovery. Still, it is helpful to have a `Parser` definition
for it in order to auto-generate helpers such as the pretty printer. module ::=
    Parser for a Lean module. We never actually run this parser but instead use the imperative definitions below that
return the same syntax tree structure, but add error recovery. Still, it is helpful to have a `Parser` definition
for it in order to auto-generate helpers such as the pretty printer. header command*

一个模块由一个 模块头，后面跟随一系列 命令 组成。

5.3.1. 模块头🔗

模块头列出在当前模块之前需要繁释的模块。 它们的声明在当前模块中可见。

syntaxModule Headers

模块头由一系列 import 语句 组成：

header ::=
    import*

可选的 prelude 关键字只应在 Lean 源码中出现：

header ::= ...
    | prelude
      import*

如果存在 prelude 关键字，则表示该模块属于 Lean 前导库 的实现部分，也就是无需显式导入任何模块即可用到的代码——不应在 Lean 实现之外使用。

syntax前导库模块
prelude ::=
    prelude
syntax导入
import ::= ...
    | import ident

导入指定模块。 导入模块会让其内容及其递归导入的所有模块的内容在当前模块中可见。

模块与命名空间不一定一一对应。 模块可以向任意命名空间添加名称，而导入模块不会影响当前打开的命名空间集合。

被导入模块的名称会通过将名称中的点（.）替换为路径分隔符，并加上 .lean 或 .olean 后缀，转成文件名。 Lean 在其包含路径中搜索对应的中间构建产物或可导入的模块文件。

命令 是 Lean 的顶级语句。 例如归纳类型声明、定理、函数定义、像 open 或 variable 这样的命名空间修饰符，以及 #check 这样的交互查询，都是命令的例子。 命令的语法是用户可扩展的，而且命令本身还可以 扩展用于解析后续命令的语法。 各类 Lean 命令的详细说明见手册相应章节，下文不再一一枚举。

5.4. 繁释后的模块🔗

Lean 在繁释一个模块时，最终会得到一个 环境。 该环境包括本模块声明的常量、归纳类型、定理、类型类、实例 及其它所有声明，还有用于记录各种数据（如 simp 集、命名空间别名、文档注释）的辅助表。

Lean 处理模块时，命令会不断向环境中添加内容。 模块的环境可以被序列化为一个 .olean 文件，其中即包含环境，也包含环境所需的运行时对象压缩堆区。 这意味着被导入的模块无需重新执行所有命令即可被加载。

5.5. 包、库与目标🔗

Lean 模块被组织为 包，包是代码分发的单位。 一个 包 可以包含多个库或可执行文件。

包中面向其他 Lean 包复用的代码会被组织为 库。 面向编译并作为独立程序运行的代码被组织为 可执行文件。 包、库、可执行文件将在 Lake，Lean 标准构建工具 一节中详细介绍。